$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$:fpf($A$; $a$.$B$($a$)). $f$ $\in$ fpf($A$; $a$.top)